package i5.modelman.chase;

import i5.modelman.merge.dependency.Constraint;
import i5.modelman.merge.dependency.Dependency;
import i5.modelman.merge.dependency.ImplicationDirection;

import java.util.Arrays;
import java.util.HashMap;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import org.apache.log4j.Logger;

import jpl.Compound;
import jpl.JPL;
import jpl.Query;
import jpl.Term;
import jpl.Util;

public class PrologUtil {
	private static Logger logger = Logger.getLogger(PrologUtil.class);
	private static final Map<String,String> loadedPrologFiles=new HashMap<String,String>();
	public static final String FACT = "fact";
	public static final String RULE = "rule";
	
	static {
		// loading prolog source files		
		try{
			consultResourceFile("freeze.pl");
			consultResourceFile("meta.pl");
			consultResourceFile("chase.pl");
			consultResourceFile("contract.pl");
			consultResourceFile("egd.pl");
			consultResourceFile("rewrite.pl");
			
		}
		catch(ResourceNotFoundException e){
			logger.error("Prolog Source Not Loaded!");
			throw new RuntimeException(e);
		}
	}


	public static boolean consultResourceFile(String file) throws ResourceNotFoundException {
	    try {
	      if(!loadedPrologFiles.containsKey(file)) {
	        String tmpFileName = ResourceLocator.locateByTmpFile(file).replaceAll("\\\\", "\\\\\\\\");
	        if (!consult(tmpFileName)) {
	          throw new ResourceNotFoundException("Cannot load prolog file " + file);
	        }
	        loadedPrologFiles.put(file,tmpFileName);
	      }
	      else {
	        String tmpFileName = loadedPrologFiles.get(file);
	        if (!consult(tmpFileName)) {
	          throw new ResourceNotFoundException("Cannot load prolog file " + file);
	        }
	      }
	    }
	    catch(ResourceNotFoundException except) {
	      throw except;
	    }
	    catch(Exception otherException) {
	      throw new ResourceNotFoundException("Cannot load prolog file " + file, otherException);
	    }
	    return true;
	}
	
	
	
	static boolean consult(String file) {
		return booleanQuery("consult('" + file + "').");
	}


	
	public static void addFact(Term t) {
		booleanQuery("addFact(" +  t.toString() + ").");
	}

	
	public static boolean booleanQuery(String query){
		logger.debug(query);
		return Query.hasSolution(query);
	}
	
	public static Iterator<Term> factIterator() {
		final Hashtable[] solutions = Query.allSolutions(FACT + "(X)");
		
		return new Iterator<Term>(){
			private int index = 0;
			public boolean hasNext() {
				return solutions != null && index < solutions.length;
			}

			public Term next() {
				Hashtable solution = solutions[index++];
				return (Term) solution.values().iterator().next();
			}

			public void remove() {
				throw new UnsupportedOperationException();
			}
			
		};
	}
	
	public static boolean isFact(String fact){
		return booleanQuery(FACT + "(" + fact + ")");
	}
	
//	/**
//	 * This is a work-around for old class of Position.
//	 * You should call <code>isBuiltinPredicate(String, int)</code> instead!
//	 * @deprecated
//	 * @param predicateName
//	 * @return
//	 */
//	public static boolean isBuiltinPredicate(String predicateName){
//		int arity = getArityOf(predicateName);
//		return isBuiltinPredicate(predicateName, arity);
//	}
	
	public static boolean isBuiltinPredicate(String predicate, int arity){
		String predID =  "(" + predicate + ")/" + arity;
		return booleanQuery("is_built_in(" + predID + ")");
	}
	
	public static void clearFacts(){
		booleanQuery("clearFacts.");
	}
	
	public static void clearKB(){
		booleanQuery("clearKnowledgeBase.");
//		clearArityCache();
	}

//	private static void clearArityCache() {
//		name2Arity.clear();
//	}



	public static void clearRules() {
		booleanQuery("clearRules.");
	}

	public static void tellConstraint(Constraint c) {
		if(isEGD(c)){
			tellEGD(c);
		}
		else {
			tellTGD(c);
		} 
	}
	
	private static boolean isEGD(Constraint c) {
		Query head;
		if(c.getDirection().equals(ImplicationDirection.RIGHT_TO_LEFT)){
			head = c.getLhs();
		
		}
		else if(c.getDirection().equals(ImplicationDirection.LEFT_TO_RIGHT)){
			head = c.getRhs();
		}
		else{
			return false;
		}
		String predicate = head.goal().name();
		if(predicate.equals("equal")) return true;
		
		return predicate.equals(",") && head.goal().arg(1).name().equals("equal");
	}

	public static void tellRewritingTGD(Constraint c){
		booleanQuery("tell_rewriting_rule("+ toCrudeString(c) +").");
	}
	

	public static void tellEGD(Constraint c){
		booleanQuery("tell_egd("+ toCrudeString(c) +").");
	}
	public static void tellTGD(Constraint c){
		booleanQuery("tell_tgd("+ toCrudeString(c) +").");
	}

	public static String queryToCrudeString(Query q){
		Compound goal = q.goal();
		return termToCrudeString(goal);
	}
	
	private static String termToCrudeString(Term t) {
		if (t.name().equals(",")) {
			String s = "','(";
			for (int i = 1; i <= t.arity(); ++i) {// note Term.arg(int) counts
													// from 1.
				s += termToCrudeString(t.arg(i));
				if (i != t.arity()) {
					s += ", ";
				}
			}
			
			return s + ")";
		} else {
			return t.toString();
		}
	}

	

	
	public static String freeze(String predName, int arity){
		String frozen = "Frozen";
		String query = "freeze_predicate(" + predName +"," + arity + "," + frozen + ").";
		Hashtable solution = Query.oneSolution(query);
		Compound result = (Compound) solution.get(frozen);
		
		return result.toString();
	
	}


	public static String[][] allSolutions(String query, String... variables){
		try{
			int numOfVars = variables.length;
			Hashtable[] solutions = allSolutions(query);
			String[][] result  = new String[solutions.length][numOfVars];
			for(int i = 0; i < solutions.length; i++){
				for(int j = 0; j < numOfVars; j++){
					result[i][j] =  solutions[i].get(variables[j]).toString();
				}
			}
			return result;
		}
		catch(Exception e){
			throw new RuntimeException("Error while executing query " + query, e);
		}
	}
	private static Hashtable[] allSolutions(String query){
		return Query.allSolutions(query);
	}
	

	static Integer queryPrologForArity(String predicate) {
		String arity = "Arity";
		String query = "current_functor("+ predicate + "," + arity + ").";
		Hashtable solution = Query.oneSolution(query);
		return ((jpl.Integer) solution.get(arity)).intValue();
	}



	public static Tableau createTableauFromProlog() {
		Tableau t = new Tableau();
		t.loadFromProlog();
		return t;
	}

	public static void tellConstraints(Iterable<? extends Constraint> constraints) {
		for(Constraint c : constraints){
			tellConstraint(c);
		}
	}

	public static void tellDependency(Dependency dependency) {
		Iterator<Constraint> it = dependency.getConstraints();
		while(it.hasNext()){
			tellConstraint(it.next());
		}
	}

	public static int ruleCount(){
		return ((jpl.Integer)new Query("countRule(X)").oneSolution().get("X")).intValue();
	}

	public static void clearProjectionRules() {
		booleanQuery("clearProjectionRules.");
	}



	public static void tellProjectionRules(Dependency dependency) {
		Iterator<Constraint> it = dependency.getConstraints();
		while(it.hasNext()){
			Constraint c  = it.next();
			booleanQuery("tellProjectionRule(" + toCrudeString(c) + ").");	
		}
		
	}

	public static String toCrudeString(Constraint c){
		return c.getDirection().text + "(" + queryToCrudeString(c.getLhs()) + "," + queryToCrudeString(c.getRhs()) +")";
	}

	public static String constraintToFlattenedString(Constraint c){
		return queryToFlattenedString(c.getLhs()) + c.getDirection().text + queryToFlattenedString(c.getRhs());
	}
	
	public static String queryToFlattenedString(Query q) {
		Compound goal = q.goal();
		return termToString(goal);
	}
	
	public static String termToString(Term t) {
		if (t.name().equals(",")) {
			String s = "";
			for (int i = 1; i <= t.arity(); ++i) {// note Term.arg(int) counts
													// from 1.
				s += termToString(t.arg(i));
				if (i != t.arity()) {
					s += ", ";
				}
			}
			return s;
		} else {
			return t.toString();
		}
	}
	
	
//	@Deprecated
//	static Map<String, Integer> name2Arity = new HashMap<String, Integer>();// FIXME: should be removed from utility class
//
//	public static void clearName2Arity(){
//		name2Arity.clear();
//	}
//
//	@Deprecated
//	public static int getArityOf(String predicate) {
//		Integer arity = null;
////			name2Arity.get(predicate);
//		if (arity == null) {
//			arity = queryPrologForArity(predicate);
////			name2Arity.put(predicate, arity);
//		}
//		return arity;
//	}
//
//
//
//	/**
//	 * For testing only!
//	 * @param pred
//	 * @param arity
//	 */
//	public static void putArity(String pred, int arity){
//		name2Arity.put(pred, arity);
//	}



	public static void tellHelper(String helperRule) {
		Term t = Util.textToTerm(helperRule);
		booleanQuery("tell_helper("+ t.toString() +").");
	}


	/**
	 * It materializes a tuple with all distinct skolem variables.
	 * 
	 * @param relationName
	 * @param arity
	 */
	public static Compound skolemize(String relationName, Integer arity) {
		String skolemized = "SkolemizedPred";
		String query = "skolem_predicate(" + relationName +"," /*+ arity + ","*/ + arity  +"," +skolemized +").";
		Hashtable solution = Query.oneSolution(query);
		Compound result = (Compound) solution.get(skolemized);
		
		return result;
	}



//	public static void tellHelpers(List<InvertibleFunctor> helpers) {
//		for(InvertibleFunctor inv : helpers){
//			for(String helperRule : inv.toRules()){
//				tellHelper(helperRule);
//			}
//		}
//	}
	
	
}
